\begin{tabbing}
@$i$ \=$k$(v:$T$) triggers local action $a$\+
\\[0ex]when $P$ ($x$:$A$) v
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(vartype($i$;$x$) $\subseteq$r $A$) \& $\forall$$e$@$i$. (kind($e$) = $k$) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$)\+
\\[0ex]\& \=$\forall$${\it e'}$@$i$.\+
\\[0ex](kind(${\it e'}$) = locl($a$))
\\[0ex]$\Rightarrow$ ($\exists$$e$:E. (($e$ $<$loc ${\it e'}$) \& kind($e$) = $k$ \& ($\uparrow$($P$(($x$ when $e$),val($e$))))))
\-\\[0ex]\& $\forall$$e$@$i$. (kind($e$) = $k$) $\Rightarrow$ ($\uparrow$($P$(($x$ when $e$),val($e$)))) $\Rightarrow$ $\exists$${\it e'}$@$i$.kind(${\it e'}$) = locl($a$)
\-
\end{tabbing}